perm filename NOTES[W80,JMC] blob sn#492913 filedate 1980-01-15 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Ketonen's proof procedure
C00003 ENDMK
CāŠ—;
Ketonen's proof procedure
I was probably much too sketchy in describing how to use my decision procedure.
In more detail:
   R MMFOL
   (DSKIN (DIRECT.LSP))
   (FOO)
   FETCH DIR.TST;
   ASSUME <fla to be tested>;
   REFLECT DEC,<the line no>;
dir.lsp[1,jk] Ketonen's proof procedure